i:Id, ds:x:Id fp Type, da:k:Knd fp Type, x:Id, T:Type, ks:Knd List,
tr:(k:{k:Knd| (k  ks) }State(ds)Valtype(da;k)TT).
ds || x : T  (k:Knd. k  dom(R-da(R-state-var(i;ds;da;x;T;ks;tr);i))  (k  ks)) 

latex

Definitions

False, P  Q, A, Void, t  T, x:A. B(x), Top, x. t(x), x:A. B(x), x:AB(x), x  dom(f), b, (x  l), Id, Prop, b, , x:AB(x), P & Q, P  Q, Unit, left+right, <a,b>, type List, State(ds), {x:A| B(x) }, IdDeq, f || g, , Valtype(da;k), x : v, KindDeq, f  g, x.A(x), reduce(f;k;as), a = b, if b t else f fi, R-state-var(i;ds;da;x;T;ks;tr), R-da(R;i), Type, Knd, a:A fp B(a), s = t, {T}, P  Q, P  Q

Lemmas

false wf, fpf-join-dom-sq, assert of bor, cons member, fpf-single-dom, R-da wf, R-state-var wf, fpf-compatible wf, id-deq wf, decl-state wf, l member wf, fpf-trivial-subtype-top, R-state-var-da, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, not wf, Id wf, assert wf, fpf-dom wf, reduce wf, fpf-join wf, fpf-single wf, ma-valtype wf, Kind-deq wf, fpf wf, fpf-empty wf, top wf, Knd wf